Nuprl Lemma : weak-antecedent-surjection-property
11,40
postcript
pdf
es
:ES,
P
,
Q
:(E
),
f
:({
e
:E|
P
(
e
)}
E).
Q
=
f
==
P
(
f
{
e
:E|
P
(
e
)}
{
e
:E|
Q
(
e
)} )
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
P
&
Q
,
Q
=
f
==
P
,
E
,
f
(
a
)
,
{
x
:
A
|
B
(
x
)}
,
x
:
A
B
(
x
)
,
S
T
,
suptype(
S
;
T
)
,
Type
,
,
ES
Lemmas
weak-antecedent-function-property
origin
es:ES, P, Q:(E
), f:({e:E| P(e)} E). Q 
= f== P 
(f 
{e:E| P(e)} {e:E| Q(e)} ) es:ES, P, Q:(E), f:({e:E| P(e)} E). Q = f== P (f {e:E| P(e)} {e:E| Q(e)} ) T Qx:A. B(x)
B(x)= f== PB(x)
T